﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework.Goals;
using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace MicroBenchmarks.MultiMethodsInLoop
{
    [PexClass]    
    [TestClass]
    public partial class MultiMethodsInLoopTest
    {
        /// <summary>
        /// An example state that can be achived by calling IncrM1 5 times. However, for calling IncrM1,
        /// there is a pre-condition that some other method has to be called. An FSM with multiple loops 
        /// is required to iterate those many loops
        /// 
        /// Current Result: The call-back is not getting invoked. Needs to debug. One reason could be 
        /// that not even a single test is generated...Pex Issue.
        /// </summary>
        /// <param name="ifd"></param>                        
        [PexMethod]
        [PexMe.Attribute.FieldAccessObserver]
        [PexMe.Attribute.InsufficientObjectFactoryObserver]
        public void FieldTest1([PexAssumeUnderTest]MultiMethodsInLoop ifd)
        {         
            if (ifd.InternalState)
                PexAssert.ReachEventually();
        }
    }
}
